Nuprl Lemma : csinput-cmd_wf
11,40
postcript
pdf
Cmd
:Type,
x
:chain_sys(
Cmd
). (
csinput?(
x
))
(csinput-cmd(
x
)
Cmd
)
latex
Definitions
s
=
t
,
t
T
,
False
,
Type
,
Id
,
type
List
,
x
:
A
B
(
x
)
,
P
Q
,
True
,
chain
sys
ind
csupdate
compseq
tag
def
,
b
,
csinput?(
x
)
,
chain
sys
ind
csinput
compseq
tag
def
,
x
:
A
B
(
x
)
,
left
+
right
,
chain_sys(
Cmd
)
,
csinput-cmd(
x
)
,
x
:
A
.
B
(
x
)
Lemmas
assert
wf
,
csinput?
wf
,
chain
sys
wf
,
true
wf
,
false
wf
origin
Cmd:Type, x:chain_sys(Cmd). (
csinput?(x)) 
(csinput-cmd(x) 
Cmd) Cmd:Type, x:chain_sys(Cmd). (csinput?(x)) (csinput-cmd(x) Cmd) T
B(x) Qb
B(x)x:A. B(x)